A,B:es_realizer{i:l}. R-compat{i:l}(A; B)  prop{i':l} 

latex

Definitions

ge(i; j), False, A, A  B, x. t(x), ff, tt, P  Q, if b then t else f fi , Y, P  Q, R-compat{i:l}(A; B), prop{i:l}, t  T, x:A. B(x), , x(s), guard(T), P  Q, Unit, , ,

Lemmas

ge wf, nat properties, R-interface-compat wf, not functionality wrt iff, R-discrete compat wf, R-frame-compat wf, Rda wf, Kind-deq wf, Knd wf, Rds wf, id-deq wf, fpf-compatible wf, R-base-domain wf, eq bd wf, assert-eq-id, Id wf, R-loc wf, eq id wf, true wf, Rnone? wf, assert of bnot, eqff to assert, not wf, bnot wf, assert wf, iff transitivity, Rplus-right wf, Rplus-left wf, R-size-decreases, eqtt to assert, bool wf, Rplus? wf, le wf, es realizer wf, nat plus wf, R-size wf, nat wf